Nuprl Lemma : es-init-elim
11,40
postcript
pdf
es
:event_system{i:l},
e
:es-E(
es
). (
es-first(
es
;
e
))
sqequal(es-init(
es
;
e
);
e
)
latex
Definitions
False
,
P
Q
,
A
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
P
Q
,
P
Q
,
b
,
,
s
=
t
,
t
T
,
Unit
,
left
+
right
,
es-init(
es
;
e
)
,
es-E(
es
)
,
event_system{i:l}
Lemmas
eqtt
to
assert
,
iff
transitivity
,
eqff
to
assert
,
can-apply-pred?
,
assert
of
bnot
origin
es:event_system{i:l}, e:es-E(es). (
es-first(es; e)) 
sqequal(es-init(es;e); e) es:event_system{i:l}, e:es-E(es). (es-first(es; e)) sqequal(es-init(es;e); e) Q
A
B(x)x:A. B(x)
B(x)
Q
Qb
T